D:Dsys, n:, L:(Id(MsgA List)).
(loc:Id. (A,BL(loc).A ||+ B))
 (loc:Id. ||L(loc)|| = n)
 (m:n. D  loc.L(loc)[m]  D  loc.(L(loc))) 

latex

Definitions	Dsys, t  T, , MsgA, Id, x:A. B(x), A ||+ B, Prop, x(s), x,y. t(x;y), (x,yL.P(x;y)), ||as||, ij, P  Q, False, A, AB, {i..j}, D1  D2, M(i), (L), M1  M2, P & Q, i  j < k, True, T, l[i], (x  l)
Lemmas	select member, ma-sub-join-list, ma-sub transitivity, select wf, ma-join-list wf, le wf, d-sub wf, int seg wf, non neg length, length wf1, pairwise wf, ma-compat wf, Id wf, msga wf, nat wf, dsys wf